Step of Proof: subtype-top
11,40
postcript
pdf
Inference at
*
I
of proof for Lemma
subtype-top
:
T
:Type. (
T
r Top)
True
latex
by Auto THEN D 0 THEN Auto
latex
.
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
True
,
t
T
,
Top
Lemmas
true
wf
,
top
wf
origin
T:Type. (T 
r Top) 
True
by Auto THEN D 0 THEN Auto
. T:Type. (T r Top) True
by Auto THEN D 0 THEN Auto
.x:A. B(x) Q Q Q
T